\font\magtenrm=cmr10 scaled\magstep1
\pageno=8
\footline={\hss\magtenrm\folio\hss} % to graft onto previous (magnified) pages!

% this is copied from WEBMAC, with minor variations
\parskip 0pt % no stretch between paragraphs
\parindent 1em % for paragraphs and for the first line of Pascal text

\font\eightrm=cmr8
\let\sc=\eightrm \let\mainfont=\tenrm
\font\titlefont=cmr7 scaled\magstep4 % title on the contents page
\font\ttitlefont=cmtt10 scaled\magstep2 % typewriter type in title
\font\tentex=cmtex10 % TeX extended character set (used in strings)

\def\\#1{\hbox{\it#1\/\kern.05em}} % italic type for identifiers
\def\|#1{\hbox{$#1$}} % one-letter identifiers look a bit better this way
\def\
{\hbox{\bf#1\/}} % boldface type for reserved words
\def\.#1{\hbox{\tentex % typewriter type for strings
  \let\\=\BS % backslash in a string
  \let\'=\RQ % right quote in a string
  \let\`=\LQ % left quote in a string
  \let\{=\LB % left brace in a string
  \let\}=\RB % right brace in a string
  \let\~=\TL % tilde in a string
  \let\ =\SP % space in a string
  \let\_=\UL % underline in a string
  \let\&=\AM % ampersand in a string
  #1}}
\def\#{\hbox{\tt\char`\#}} % parameter sign
\def\${\hbox{\tt\char`\$}} % dollar sign
\def\%{\hbox{\tt\char`\%}} % percent sign
\def\↑{\ifmmode\mathchar"222 \else\char`↑ \fi} % pointer or hat
% circumflex accents can be obtained from \↑↑D instead of \↑
\def\AT!{@} % at sign for control text

\chardef\AM=`\& % ampersand character in a string
\chardef\BS=`\\ % backslash in a string
\chardef\LB=`\{ % left brace in a string
\def\LQ{{\tt\char'22}} % left quote in a string
\chardef\RB=`\} % right brace in a string
\def\RQ{{\tt\char'23}} % right quote in a string
\def\SP{{\tt\char`\ }} % (visible) space in a string
\chardef\TL=`\~ % tilde in a string
\chardef\UL=`\_ % underline character in a string

\newbox\bak \setbox\bak=\hbox to -1em{} % backspace one em
\newbox\bakk\setbox\bakk=\hbox to -2em{} % backspace two ems

\newcount\ind % current indentation in ems
\def\1{\global\advance\ind by1\hangindent\ind em} % indent one more notch
\def\2{\global\advance\ind by-1} % indent one less notch
\def\3#1{\hfil\penalty#10\hfilneg} % optional break within a statement
\def\4{\copy\bak} % backspace one notch
\def\5{\hfil\penalty-1\hfilneg\kern2.5em\copy\bakk\ignorespaces}% optional break
\def\6{\ifmmode\else\par % forced break
  \hangindent\ind em\noindent\kern\ind em\copy\bakk\ignorespaces\fi}
\def\7{\Y\6} % forced break and a little extra space

\let\yskip=\smallskip
\def\to{\mathrel{.\,.}} % double dot, used only in math mode
\def\note#1#2.{\Y\noindent{\hangindent2em\baselineskip10pt\eightrm#1 #2.\par}}
\def\lapstar{\rlap{*}}
\def\startsection{\Q\noindent{\let\*=\lapstar\bf\modstar.\quad}}
\def\defin#1{\global\advance\ind by 2 \1\&{#1 }} % begin `define' or `format'
\def\A{\note{See also}} % cross-reference for multiply defined section names
\def\B{\mathopen{\.{@\{}}} % begin controlled comment
\def\C#1{\ifmmode\gdef\XX{\null$\null}\else\gdef\XX{}\fi % Pascal comments
  \XX\hfil\penalty-1\hfilneg\quad$\{\,$#1$\,\}$\XX}
\def\D{\defin{define}} % macro definition
\def\E{\cdot10↑} % exponent in floating point constant
\def\F{\defin{format}} % format definition
\let\G=\ge % greater than or equal sign
\def\H#1{\hbox{\rm\char"7D\tt#1}} % hexadecimal constant
\let\I=\ne % unequal sign
\def\J{\.{@\&}} % TANGLE's join operation
\def\K{\;\mathrel{:=}\;\30} % colon-equal
\let\L=\le % less than or equal sign
\outer\def\M#1.{\MN#1.\ifon\vfil\penalty-100\vfilneg % beginning of section
  \vskip12ptminus3pt\startsection\ignorespaces}
\outer\def\N#1.#2.{\MN#1.\vfil\eject % beginning of starred section
  \def\rhead{\uppercase{\ignorespaces#2}} % define running headline
  \message{*\modno} % progress report
  \edef\next{\write\cont{\Z{#2}{\modno}{\the\pageno}}}\next % to contents file
  \ifon\startsection{\bf\ignorespaces#2.\quad}\ignorespaces}
\def\MN#1.{\par % common code for \M, \N
  {\xdef\modstar{#1}\let\*=\empty\xdef\modno{#1}}
  \ifx\modno\modstar \onmaybe \else\ontrue \fi \mark{\modno}}
\def\O#1{\hbox{\rm\char'23\kern-.2em\it#1\/\kern.05em}} % octal constant
\def\P{\rightskip=0pt plus 100pt minus 10pt % go into Pascal mode
  \sfcode`;=3000
  \pretolerance 10000
  \hyphenpenalty 10000 \exhyphenpenalty 10000
  \global\ind=2 \1\ \unskip}
\def\Q{\rightskip=0pt % get out of Pascal mode
  \sfcode`;=1500 \pretolerance 200 \hyphenpenalty 50 \exhyphenpenalty 50 }
\let\R=\lnot % logical not
\let\S=\equiv % equivalence sign
\def\T{\mathclose{\.{@\}}}} % terminate controlled comment
\def\U{\note{This code is used in}} % cross-reference for uses of sections
\let\V=\lor % logical or
\let\W=\land % logical and
\def\X#1:#2\X{\ifmmode\gdef\XX{\null$\null}\else\gdef\XX{}\fi % section name
  \XX$\langle\,$#2{\eightrm\kern.5em#1}$\,\rangle$\XX}
\def\Y{\par\medskip}
\let\Z=\let % now you can \send the control sequence \Z
\def\){\hbox{\.{@\$}}} % sign for string pool check sum
\def\]{\hbox{\.{@\\}}} % sign for forced line break
\def\=#1{\kern2pt\hbox{\vrule\vtop{\vbox{\hrule
        \hbox{\strut\kern2pt\.{#1}\kern2pt}}
      \hrule}\vrule}\kern2pt} % verbatim string
\let\~=\ignorespaces
\let\*=*

\thickmuskip=\thinmuskip

\def\T{{|\!-}\;}
\font\ninebf=cmbx9

\noindent {\bf Appendix: Example of a {\ninebf CHEX} script.}

\medskip
\P\6
\4$\\{bool}\K\#$: \37\\{atom}.\C{there's a special kind of atom called a %
\\{bool}}\6
\4$\\{proof}(\|b:\\{bool})\K\#$: \37\\{atom}.\C{and another called a \\{proof}
of a \\{bool}; logicians say $\T b$}\par
\Y\6
\4$\\{eq}(\|a:\\{atom};\,\35\|x,\39\|y:\|a)\K\#$: \37\\{bool}.\C{\\{eq}
is a proposition that two variables of type \|a are equal}\6
\4$\\{is}(\|a:\\{atom};\,\35\|x,\39\|y:\|a)\K\\{proof}(\\{eq}(\|a,\39\|x,\39%
\|y))$: \37\\{atom}.\C{this asserts that $\|x=\|y$ can be proved}\6
\4$\\{identical}(\|a:\\{atom};\,\35\|x:\|a)\K\#$: \37$\\{is}(\|a,\39\|x,\39%
\|x).$\C{an axiom: $\T x=x$}\6
\4$\\{eq\_axiom}(\|a:\\{atom};\,\35\|x,\39\|y,\39\|z:\|a;\,\35\|p:\\{is}(\|a,%
\39\|x,\39\|z);\,\35\|q:\\{is}(\|a,\39\|y,\39\|z))\K\#$: \37$\\{is}(\|a,\39\|x,%
\39\|y).$\C{another axiom: if $\T x=z$ and $\T y=z$ then $\T x=y$}\6
\4$\\{eq\_symmetry}(\|a:\\{atom};\,\35\|x,\39\|y:\|a;\,\35\|p:\\{is}(\|a,\39%
\|x,\39\|y))\K\\{eq\_axiom}(\|a,\39\|y,\39\|x,\39\|y,\39\\{identical}(\|a,\39%
\|y),\39\|p)$: \37$\\{is}(\|a,\39\|y,\39\|x).$\C{previous axioms are used here
to deduce $\T y=x$ from $\T x=y$}\6
\4$\\{eq\_transitivity}(\|a:\\{atom};\,\35\|x,\39\|y,\39\|z:\|a;\,\35\|p:%
\\{is}(\|a,\39\|x,\39\|y);\,\35\|q:\\{is}(\|a,\39\|y,\39\|z))\K\\{eq\_axiom}(%
\|a,\39\|x,\39\|z,\39\|y,\39\|p,\39\\{eq\_symmetry}(\|a,\39\|y,\39\|z,\39%
\|q))$: \37$\\{is}(\|a,\39\|x,\39\|z).$\C{$\T x=y$ and $\T y=z$ implies $\T
x=z$}\6
\4$\\{eq\_functionality}(\|a,\39\|b:\\{atom};\,\35\|x,\39\|y:\|a;\,\35\|p:%
\\{is}(\|a,\39\|x,\39\|y);\,\35\|f:(\|x:\|a)\,\|b\,)\K\#$: \37$\\{is}(\|b,\39\|f(%
\|x),\39\|f(\|y)).$\C{$\T x=y$ implies $\T f(x)=f(y)$ for any function \|f}\par
\Y\6
\4$\\{nat}\K\#$: \37\\{atom}.\C{another primitive atom, representing the
nonnegative integers}\6
\4$0\K\#$: \37\\{nat}.\C{0 is a nonnegative integer by definition}\6
\4$\\{succ}(\|x:\\{nat})\K\#$: \37\\{nat}.\C{the successor function}\6
\4$\\{succ\_unique}(\|x,\39\|y:\\{nat};\,\35\|p:\\{is}(\\{nat},\39\\{succ}(%
\|x),\39\\{succ}(\|y)))\K\#$: \37$\\{is}(\\{nat},\39\|x,\39\|y).$\C{another
axiom: different \\{nat}s can't have the same \\{succ}}\6
\4$\\{nat\_pred}(\|x:\\{nat})\K\\{bool}$: \37\\{atom}.\C{a predicate defined on
\\{nat}s}\6
\4$\\{nat\_imp}(\|p:\\{natpred};\,\35\|x:\\{nat};\,\35\|q:\\{proof}(\|p(\|x)))%
\K\\{proof}(\|p(\\{succ}(\|x)))$: \37\\{atom}.\C{an inductive implication}\6
\4$\\{induction}(\|p:\\{nat\_pred};\,\35\|q:\\{proof}(\|p(0));\,\35\|r:\\{nat%
\_imp}(\|p))\K\#$: \37$(\|x:\\{nat})\\{proof}(\|p(\|x)).$\C{Peano's axiom}\par
\Y\6
\4$\\{sum}(\|x,\39\|y:\\{nat})\K\#$: \37\\{nat}.\C{the sum of two \\{nat}s is a
\\{nat}}\6
\4$\\{sum\_ax1}(\|x:\\{nat})\K\#$: \37$\\{is}(\\{nat},\39\\{sum}(\|x,\390),\39%
\|x).$\C{$\T x+0\;=\;x$}\6
\4$\\{sum\_ax2}(\|x,\39\|y:\\{nat})\K\#$: \37$\\{is}(\\{nat},\39\\{sum}(\|x,\39%
\\{succ}(\|y)),\39\\{succ}(\\{sum}(\|x,\39\|y))).$\C{$\T x+y'\;=\;(x+y)'$}\par
\Y\6
\4$\\{thm1}(\|x,\39\|y:\\{nat})\K\\{eq}(\\{nat},\\{sum}(\\{succ}(\|x),\39\|y),\39%
\\{succ}(\\{sum}(\|x,\39\|y)))$: \37\\{bool}.\C{$x'+y\;=\;(x+y)'$}\6
\4$\\{step1}(\|x:\\{nat})\K\\{sum\_ax1}(\\{succ}(\|x))$: \37$\\{is}(\\{sum}(%
\\{succ}(\|x),\390),\39\\{succ}(\|x)).$\C{$\T x'+0\;=\;x'$}\6
\4$\\{step2}(\|x:\\{nat})\K\\{eq\_functionality}(\\{nat},\39\\{nat},\39\\{sum}(%
\|x,\390),\39\|x,\39\\{sum\_ax1}(\|x),\39\\{succ})$: \37$\\{is}(\\{succ}(%
\\{sum}(\|x,\390)),\39\\{succ}(\|x)).$\C{$\T (x+0)'\;=\;x'$}\6
\4$\\{step3}(\|x:\\{nat})\K\\{eq\_axiom}(\\{nat},\39\\{sum}(\\{succ}(\|x),%
\390),\39\\{succ}(\\{sum}(\|x,\390)),\39\\{succ}(\|x),\39\\{step1}(\|x),\39%
\\{step2}(\|x))$: \37$\\{proof}(\\{thm1}(\|x,\390)).$\C{hence $\T x'+0\;=\;(x+0)'$}%
\6
\4$\\{step4}(\|x,\39\|y:\\{nat};\,\35\|q:\\{proof}(\\{thm1}(\|x,\39\|y)))\K\3{-100}%
\\{eq\_axiom}(\\{nat},\39\\{sum}(\\{succ}(\|x),\39\|y),\39\\{sum}(\|x,\39%
\\{succ}(\|y)),\39\\{sum}(\|x,\39\|y),\39\|q,\39\\{sum\_ax2}(\|x,\39\|y))$: %
\37$\\{is}(\\{sum}(\\{succ}(\|x),\39\|y),\39\\{sum}(\|x,\39\\{succ}(\|y))).$%
\C{assuming \\{thm1} as an induction hypothesis, we can prove that $x'+y\;=\;x+y'$}%
\6
\4$\\{step5}(\|x,\39\|y:\\{nat};\,\35\|q:\\{proof}(\\{thm1}(\|x,\39\|y)))\K%
\\{eq\_functionality}(\\{nat},\39\\{nat},\39\\{sum}(\\{succ}(\|x),\39\|y),\39%
\\{sum}(\|x,\39\\{succ}(\|y)),\39\\{step4}(\|x,\39\|y,\39\|q),\39\\{succ})$: %
\37$\\{is}(\\{succ}(\\{sum}(\\{succ}(\|x),\39\|y)),\39\\{succ}(\\{sum}(\|x,\39%
\\{succ}(\|y)))).$\C{from which it follows that $(x'+y)'\;=\;(x+y')'$}\6
\4$\\{step6}(\|x,\39\|y:\\{nat})\K\\{sum\_ax2}(\\{succ}(\|x),\39\|y)$: \37$%
\\{is}(\\{sum}(\\{succ}(\|x),\39\\{succ}(\|y)),\39\\{succ}(\\{sum}(\\{succ}(%
\|x),\39\|y))).$\C{and $x'+y'\;=\;(x'+y)'$ by definition}\6
\4$\\{step7}(\|x,\39\|y:\\{nat};\,\35\|q:\\{proof}(\\{thm1}(\|x,\39\|y)))\K%
\\{eq\_transitivity}(\\{nat},\39\\{sum}(\\{succ}(\|x),\39\\{succ}(\|y)),\39%
\\{succ}(\\{sum}(\\{succ}(\|x),\39\|y)),\39\\{succ}(\\{sum}(\|x,\39\\{succ}(%
\|y))),\39\\{step6}(\|x,\39\|y),\39\\{step5}(\|x,\39\|y,\39\|q))$: \37$%
\\{proof}(\\{thm1}(\|x,\39\\{succ}(\|y))).$\C{hence the induction hypothesis
yields $x'+y'\;=\;(x+y')'$ as desired}\6
\4$\\{qed\_thm1}(\|x:\\{nat})\K\\{induction}(\\{thm1}(\|x),\39\\{step3}(\|x),%
\39\\{step7}(\|x))$: \37$(\|y:\\{nat})\\{proof}(\\{thm1}(\|x,\39\|y)).$\par
\Y\6
\4$\\{thm2}(\|x,\39\|y:\\{nat})\K\\{eq}(\\{nat},\\{sum}(\|x,\|y),\39%
\\{sum}(\|y,\|x)))$: \37\\{bool}.\C{$x+y\;=\;y+x$}\6
\bigskip
\noindent(The reader may now wish to construct a proof of \\{thm2}.)
\bye